
Types, Values, and Effects

* Evaluation and Execution

** Imperative model of computation

Programs are a sequence of COMMANDS

A command 1) Examines the contents of memory
          2) Performs a simple computation 
          3) Modifies the memory
          4) Continues with the next instruction
  
Commands are executed for their EFFECT on the memory (IO, Network)

** ML model of computation

Computation by EVALUATION OF EXPRESSIONS rather than EXECUTION OF
COMMANDS

f(x) = 2 x^2 + x + 1

*** Advantages

Close relationship to math = easier mathematical techniques for
reasoning

commands as a special case

* ML Computation Model

Expressions

1) May or may not have a TYPE
2) May or may not have a VALUE
3) May or may not cause an EFFECT

Type is a description of the value an expresion yields (if it yields
one at all)

Ex:  If e : int, value is a number
        e : float, value is a floating point number

Type is a PREDICTION of the form of the value

Every expression has at least one type.  
 - Those that do are WELL-TYPED
 - Those that do not are ILL-TYPED.  Ineligible for evaluation.
 - TYPE-CHECKER tells which expressions are well or ill typed

A well-typed expression is evaluated to determine its value if it has one

  It may not have a value if
   - nontermination
   - exception 

  If it has a value
  - type bool => true or false, cannot be 7, 3.14

An expression may also cause an effect

 - Exception
 - Modifying memory
 - IO

Type says nothing about effects!!

For us, no effects for awhile

** Type Checking

*** What is a type?

1) A NAME for the type
2) The VALUES of the type
3) The OPERATIONS on the values of the type 

*** What types are there

INT

Name: int
Values: 0, 1, -1, 2
Operations: + - * / div mod

1 + 3 mod 5

Formation of expressions is governed by TYPING RULES

-----------
 1 : int

 n : int    m : int
--------------------
 n + m : int


          -------   -------
          3 : int   5 : int
-------   -----------------
1 : int   3 mod 5 : int
-----------------------
1 + 3 mod 5 : int
 
** Evaluation

5 --> 5
2 + 3 --> 5 

n --> N  m --> M   N + M = k   
-----------------------------
n + m --> k

* Types, Types, Types

** Float

 - Values: 3.14
 - Operations: +.

** Char

 - Values: 'c'
 - Ops: code, <

** String

 - Values: "Sean"
 - Ops: ^ length 

** Bool
  
 - Values: true, false
 - Ops: && , if .. then .. else


e1 : bool  e2 : tau  e3 : tau
----------------------------
if e1 then e2 else e3 : tau


 e1 --> true   e2 --> e
--------------------------
if e1 then e2 else e3 --> e

 e1 --> false   e3 --> e
--------------------------
if e1 then e2 else e3 --> e


Now we have more than one type, enough rope to hang ourselves!

2 + "sean"

if true then 5 else 4 + "sean"
